Step of Proof: sq_stable__and
9,38
postcript
pdf
Inference at
*
I
of proof for Lemma
sq
stable
and
:
P
,
Q
:
. SqStable(
P
)
SqStable(
Q
)
SqStable(
P
Q
)
latex
by ((Unfold `sq_stable` 0)
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat
C
3:n)) (first_tok :t) inil_term)))
latex
C
1
:
C1:
1.
P
:
C1:
2.
Q
:
C1:
3. (
P
)
P
C1:
4. (
Q
)
Q
C1:
5.
(
P
Q
)
C1:
P
C
2
:
C2:
1.
P
:
C2:
2.
Q
:
C2:
3. (
P
)
P
C2:
4. (
Q
)
Q
C2:
5.
(
P
Q
)
C2:
Q
C
.
Definitions
t
T
,
P
Q
,
SqStable(
P
)
,
P
Q
,
,
x
:
A
.
B
(
x
)
Lemmas
squash
wf
origin